排中律はHPM + CM₂で証明可能
1. $ \phi \lor \lnot \phi \to \bot \vdash (\phi \lor \lnot \phi \to \bot) \to (\phi \to (\phi \lor \lnot \phi \to \bot)) （$ \sf K）
2. $ \phi \lor \lnot \phi \to \bot \vdash \phi \lor \lnot \phi \to \bot （$ \sf Axm）
3. $ \phi \lor \lnot \phi \to \bot \vdash \phi \to (\phi \lor \lnot \phi \to \bot) （1.と2.の$ \sf MP）
4. $ \phi \lor \lnot \phi \to \bot \vdash \phi \to \phi \lor \lnot \phi ($ \sf I_\lor)
5. $ \phi \lor \lnot \phi \to \bot \vdash (\phi \to (\phi \lor \lnot \phi \to \bot)) \to ((\phi \to \phi \lor \lnot \phi) \to (\phi \to \bot))（$ \sf S）
6. $ \phi \lor \lnot \phi \to \bot \vdash (\phi \to \phi \lor \lnot \phi) \to (\phi \to \bot)（5.と3.の$ \sf MP）
7. $ \phi \lor \lnot \phi \to \bot \vdash \phi \to \bot（6.と4.の$ \sf MP）
8. $ \phi \lor \lnot \phi \to \bot \vdash \lnot\phi \to \phi \lor \lnot \phi（$ \sf I_\lor）
9. $ \phi \lor \lnot \phi \to \bot \vdash\phi \lor \lnot \phi（8.と7.の$ \sf MP）
10.$ \vdash (\phi \lor \lnot \phi \to \bot) \to \phi \lor \lnot \phi（演繹定理） 11.$ \vdash ((\phi \lor \lnot \phi \to \bot) \to \phi \lor \lnot \phi) \to \phi \lor \lnot \phi（$ \sf CM_2）
12.$ \vdash \phi \lor \lnot \phi（11.と10.の$ \sf MP）